(*  Title:       Category
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2016
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter "Category"

theory Category
imports Main "HOL-Library.FuncSet"
begin

  text ‹
    This theory develops an ``object-free'' definition of category loosely following
    \cite{AHS}, Sec. 3.52-3.53.
    We define the notion ``category'' in terms of axioms that concern a single
    partial binary operation on a type, some of whose elements are to be regarded
    as the ``arrows'' of the category.

    The nonstandard definition of category has some advantages and disadvantages.
    An advantage is that only one piece of data (the composition operation) is required
    to specify a category, so the use of records is not required to bundle up several
    separate objects.  A related advantage is the fact that functors and natural
    transformations can be defined simply to be functions that satisfy certain axioms,
    rather than more complex composite objects.
    One disadvantage is that the notions of ``object'' and ``identity arrow'' are
    conflated, though this is easy to get used to.  Perhaps a more significant disadvantage
    is that each arrow of a category must carry along the information about its domain
    and codomain. This implies, for example, that the arrows of a category of sets and
    functions cannot be directly identified with functions, but rather only with functions that
    have been equipped with their domain and codomain sets.

    To represent the partiality of the composition operation of a category, we assume that the
    composition for a category has a unique zero element, which we call ‹null›,
    and we consider arrows to be ``composable'' if and only if their composite is non-null.
    Functors and natural transformations are required to map arrows to arrows and be
    ``extensional'' in the sense that they map non-arrows to null.  This is so that
    equality of functors and natural transformations coincides with their extensional equality
    as functions in HOL.
    The fact that we co-opt an element of the arrow type to serve as ‹null› means that
    it is not possible to define a category whose arrows exhaust the elements of a given type.
    This presents a disadvantage in some situations.  For example, we cannot construct a
    discrete category whose arrows are directly identified with the set of \emph{all}
    elements of a given type @{typ 'a}; instead, we must pass to a larger type
    (such as @{typ "'a option"}) so that there is an element available for use as ‹null›.
    The presence of ‹null›, however, is crucial to our being able to define a
    system of introduction and elimination rules that can be applied automatically to establish
    that a given expression denotes an arrow.  Without ‹null›, we would be able to
    define an introduction rule to infer, say, that the composition of composable arrows
    is composable, but not an elimination rule to infer that arrows are composable from
    the fact that their composite is an arrow.  Having the ability to do both is critical
    to the usability of the theory.
›

  section "Partial Magmas"

  text ‹
    A \emph{partial magma} is a partial binary operation ‹C› defined on the set
    of elements at a type @{typ 'a}.  As discussed above,
    we assume the existence of a unique element ‹null› of type @{typ 'a}
    that is a zero for ‹C›, and we use ‹null› to represent ``undefined''.
    We think of the operation ‹C› as an operation of ``composition'', and
    we regard elements ‹f› and ‹g› of type @{typ 'a} as \emph{composable}
    if ‹C g f ≠ null›.
›

  type_synonym 'a comp = "'a ⇒ 'a ⇒ 'a"

  locale partial_magma =
  fixes C :: "'a comp" (infixr "⋅" 55)
  assumes ex_un_null: "∃!n. ∀f. n ⋅ f = n ∧ f ⋅ n = n"
  begin

    definition null :: 'a
    where "null = (THE n. ∀f. n ⋅ f = n ∧ f ⋅ n = n)"

    lemma null_eqI:
    assumes "⋀f. n ⋅ f = n ∧ f ⋅ n = n"
    shows "n = null"
      using assms null_def ex_un_null the1_equality [of "λn. ∀f. n ⋅ f = n ∧ f ⋅ n = n"]
      by auto
    
    lemma comp_null [simp]:
    shows "null ⋅ f = null" and "f ⋅ null = null"
      using null_def ex_un_null theI' [of "λn. ∀f. n ⋅ f = n ∧ f ⋅ n = n"]
      by auto

    text ‹
      An \emph{identity} is a self-composable element ‹a› such that composition of
      any other element ‹f› with ‹a› on either the left or the right results in
      ‹f› whenever the composition is defined.
›

    definition ide
    where "ide a ≡ a ⋅ a ≠ null ∧
                   (∀f. (f ⋅ a ≠ null ⟶ f ⋅ a = f) ∧ (a ⋅ f ≠ null ⟶ a ⋅ f = f))"

    text ‹
      A \emph{domain} of an element ‹f› is an identity ‹a› for which composition of
      ‹f› with ‹a› on the right is defined.
      The notion \emph{codomain} is defined similarly, using composition on the left.
      Note that, although these definitions are completely dual, the choice of terminology
      implies that we will think of composition as being written in traditional order,
      as opposed to diagram order.  It is pretty much essential to do it this way, to maintain
      compatibility with the notation for function application once we start working with
      functors and natural transformations.
›

    definition domains
    where "domains f ≡ {a. ide a ∧ f ⋅ a ≠ null}"

    definition codomains
    where "codomains f ≡ {b. ide b ∧ b ⋅ f ≠ null}"

    lemma domains_null:
    shows "domains null = {}"
      by (simp add: domains_def)

    lemma codomains_null:
    shows "codomains null = {}"
      by (simp add: codomains_def)

    lemma self_domain_iff_ide:
    shows "a ∈ domains a ⟷ ide a"
      using ide_def domains_def by auto

    lemma self_codomain_iff_ide:
    shows "a ∈ codomains a ⟷ ide a"
      using ide_def codomains_def by auto

    text ‹
      An element ‹f› is an \emph{arrow} if either it has a domain or it has a codomain.
      In an arbitrary partial magma it is possible for ‹f› to have one but not the other,
      but the ‹category› locale will include assumptions to rule this out.
›

    definition arr
    where "arr f ≡ domains f ≠ {} ∨ codomains f ≠ {}"

    lemma not_arr_null [simp]:
    shows "¬ arr null"
      by (simp add: arr_def domains_null codomains_null)

    text ‹
      Using the notions of domain and codomain, we can define \emph{homs}.
      The predicate @{term "in_hom f a b"} expresses ``@{term f} is an arrow from @{term a}
      to @{term b},'' and the term @{term "hom a b"} denotes the set of all such arrows.
      It is convenient to have both of these, though passing back and forth sometimes involves
      extra work.  We choose @{term "in_hom"} as the more fundamental notion.
›

    definition in_hom     ("«_ : _ → _»")
    where "«f : a → b» ≡ a ∈ domains f ∧ b ∈ codomains f"

    abbreviation hom
    where "hom a b ≡ {f. «f : a → b»}"

    lemma arrI:
    assumes "«f : a → b»"
    shows "arr f"
      using assms arr_def in_hom_def by auto

    lemma ide_in_hom [intro]:
    shows "ide a ⟷ «a : a → a»"
      using self_domain_iff_ide self_codomain_iff_ide in_hom_def ide_def by fastforce

    text ‹
      Arrows @{term "f"} @{term "g"} for which the composite @{term "g ⋅ f"} is defined
      are \emph{sequential}.
›

    abbreviation seq
    where "seq g f ≡ arr (g ⋅ f)"

    lemma comp_arr_ide:
    assumes "ide a" and "seq f a"
    shows "f ⋅ a = f"
      using assms ide_in_hom ide_def not_arr_null by metis

    lemma comp_ide_arr:
    assumes "ide b" and "seq b f"
    shows "b ⋅ f = f"
      using assms ide_in_hom ide_def not_arr_null by metis

    text ‹
      The \emph{domain} of an arrow @{term f} is an element chosen arbitrarily from the
      set of domains of @{term f} and the \emph{codomain} of @{term f} is an element chosen
      arbitrarily from the set of codomains.
›

    definition dom
    where "dom f = (if domains f ≠ {} then (SOME a. a ∈ domains f) else null)"

    definition cod
    where "cod f = (if codomains f ≠ {} then (SOME b. b ∈ codomains f) else null)"

    lemma dom_null [simp]:
    shows "dom null = null"
      by (simp add: dom_def domains_null)

    lemma cod_null [simp]:
    shows "cod null = null"
      by (simp add: cod_def codomains_null)

    lemma dom_in_domains:
    assumes "domains f ≠ {}"
    shows "dom f ∈ domains f"
      using assms dom_def someI [of "λa. a ∈ domains f"] by auto

    lemma cod_in_codomains:
    assumes "codomains f ≠ {}"
    shows "cod f ∈ codomains f"
      using assms cod_def someI [of "λb. b ∈ codomains f"] by auto

  end

  section "Categories"

  text‹
    A \emph{category} is defined to be a partial magma whose composition satisfies an
    extensionality condition, an associativity condition, and the requirement that every
    arrow have both a domain and a codomain.
    The associativity condition involves four ``matching conditions''
    (‹match_1›, ‹match_2›, ‹match_3›, and ‹match_4›)
    which constrain the domain of definition of the composition, and a fifth condition
    (‹comp_assoc'›) which states that the results of the two ways of composing
    three elements are equal.  In the presence of the ‹comp_assoc'› axiom
    ‹match_4› can be derived from ‹match_3› and vice versa.
›

  locale category = partial_magma +
  assumes ext: "g ⋅ f ≠ null ⟹ seq g f"
  and has_domain_iff_has_codomain: "domains f ≠ {} ⟷ codomains f ≠ {}"
  and match_1: "⟦ seq h g; seq (h ⋅ g) f ⟧ ⟹ seq g f"
  and match_2: "⟦ seq h (g ⋅ f); seq g f ⟧ ⟹ seq h g"
  and match_3: "⟦ seq g f; seq h g ⟧ ⟹ seq (h ⋅ g) f"
  and comp_assoc': "⟦ seq g f; seq h g ⟧ ⟹ (h ⋅ g) ⋅ f = h ⋅ g ⋅ f"
  begin

    text‹
      Associativity of composition holds unconditionally.  This was not the case in
      previous, weaker versions of this theory, and I did not notice this for some
      time after updating to the current axioms.  It is obviously an advantage that
      no additional hypotheses have to be verified in order to apply associativity,
      but a disadvantage is that this fact is now ``too readily applicable,''
      so that if it is made a default simplification it tends to get in the way of
      applying other simplifications that we would also like to be able to apply automatically.
      So, it now seems best not to make this fact a default simplification, but rather
      to invoke it explicitly where it is required.
›

    lemma comp_assoc:
    shows "(h ⋅ g) ⋅ f = h ⋅ g ⋅ f"
      by (metis comp_assoc' ex_un_null ext match_1 match_2)

    lemma match_4:
    assumes "seq g f" and "seq h g"
    shows "seq h (g ⋅ f)"
      using assms match_3 comp_assoc by auto

    lemma domains_comp:
    assumes "seq g f"
    shows "domains (g ⋅ f) = domains f"
    proof -
      have "domains (g ⋅ f) = {a. ide a ∧ seq (g ⋅ f) a}"
        using domains_def ext by auto
      also have "... = {a. ide a ∧ seq f a}"
        using assms ide_def match_1 match_3 by meson
      also have "... = domains f"
        using domains_def ext by auto
      finally show ?thesis by blast
    qed

    lemma codomains_comp:
    assumes "seq g f"
    shows "codomains (g ⋅ f) = codomains g"
    proof -
      have "codomains (g ⋅ f) = {b. ide b ∧ seq b (g ⋅ f)}"
        using codomains_def ext by auto
      also have "... = {b. ide b ∧ seq b g}"
        using assms ide_def match_2 match_4 by meson
      also have "... = codomains g"
        using codomains_def ext by auto
      finally show ?thesis by blast
    qed

    lemma has_domain_iff_arr:
    shows "domains f ≠ {} ⟷ arr f"
      by (simp add: arr_def has_domain_iff_has_codomain)

    lemma has_codomain_iff_arr:
    shows "codomains f ≠ {} ⟷ arr f"
      using has_domain_iff_arr has_domain_iff_has_codomain by auto

    text‹
      A consequence of the category axioms is that domains and codomains, if they exist,
      are unique.
›

    lemma domain_unique:
    assumes "a ∈ domains f" and "a' ∈ domains f"
    shows "a = a'"
    proof -
      have "ide a ∧ seq f a ∧ ide a' ∧ seq f a'"
        using assms domains_def ext by force
      thus ?thesis
        using match_1 ide_def not_arr_null by metis
    qed

    lemma codomain_unique:
    assumes "b ∈ codomains f" and "b' ∈ codomains f"
    shows "b = b'"
    proof -
      have "ide b ∧ seq b f ∧ ide b' ∧ seq b' f"
        using assms codomains_def ext by force
      thus ?thesis
        using match_2 ide_def not_arr_null by metis
    qed

    lemma domains_simp:
    assumes "arr f"
    shows "domains f = {dom f}"
      using assms dom_in_domains has_domain_iff_arr domain_unique by auto

    lemma codomains_simp:
    assumes "arr f"
    shows "codomains f = {cod f}"
      using assms cod_in_codomains has_codomain_iff_arr codomain_unique by auto

    lemma domains_char:
    shows "domains f = (if arr f then {dom f} else {})"
      using dom_in_domains has_domain_iff_arr domain_unique by auto

    lemma codomains_char:
    shows "codomains f = (if arr f then {cod f} else {})"
      using cod_in_codomains has_codomain_iff_arr codomain_unique by auto

    text‹
      A consequence of the following lemma is that the notion @{term "arr"} is redundant,
      given @{term "in_hom"}, @{term "dom"}, and @{term "cod"}.  However, I have retained it
      because I have not been able to find a set of usefully powerful simplification rules
      expressed only in terms of @{term "in_hom"} that does not result in looping in many
      situations.
›

    lemma arr_iff_in_hom:
    shows "arr f ⟷ «f : dom f → cod f»"
      using cod_in_codomains dom_in_domains has_domain_iff_arr has_codomain_iff_arr in_hom_def
      by auto

    lemma in_homI [intro]:
    assumes "arr f" and "dom f = a" and "cod f = b"
    shows "«f : a → b»"
      using assms cod_in_codomains dom_in_domains has_domain_iff_arr has_codomain_iff_arr
            in_hom_def
      by auto

    lemma in_homE [elim]:
    assumes "«f : a → b»"
    and "arr f ⟹ dom f = a ⟹ cod f = b ⟹ T"
    shows "T"
     using assms in_hom_def domains_char codomains_char has_domain_iff_arr
     by (metis empty_iff singleton_iff)

    text‹
      To obtain the ``only if'' direction in the next two results and in similar results later
      for composition and the application of functors and natural transformations,
      is the reason for assuming the existence of @{term null} as a special element of the
      arrow type, as opposed to, say, using option types to represent partiality.
      The presence of @{term null} allows us not only to make the ``upward'' inference that
      the domain of an arrow is again an arrow, but also to make the ``downward'' inference
      that if @{term "dom f"} is an arrow then so is @{term f}.  Similarly, we will be able
      to infer not only that if @{term f} and @{term g} are composable arrows then
      @{term "C g f"} is an arrow, but also that if @{term "C g f"} is an arrow then
      ‹f› and ‹g› are composable arrows.  These inferences allow most necessary
      facts about what terms denote arrows to be deduced automatically from minimal
      assumptions.  Typically all that is required is to assume or establish that certain
      terms denote arrows in particular homs at the point where those terms are first
      introduced, and then similar facts about related terms can be derived automatically.
      Without this feature, nearly every proof would involve many tedious additional steps
      to establish that each of the terms appearing in the proof (including all its subterms)
      in fact denote arrows.
›

    lemma arr_dom_iff_arr:
    shows "arr (dom f) ⟷ arr f"
      using dom_def dom_in_domains has_domain_iff_arr self_domain_iff_ide domains_def
      by fastforce

    lemma arr_cod_iff_arr:
    shows "arr (cod f) ⟷ arr f"
      using cod_def cod_in_codomains has_codomain_iff_arr self_codomain_iff_ide codomains_def
      by fastforce

    lemma arr_dom [simp]:
    assumes "arr f"
    shows "arr (dom f)"
      using assms arr_dom_iff_arr by simp

    lemma arr_cod [simp]:
    assumes "arr f"
    shows "arr (cod f)"
      using assms arr_cod_iff_arr by simp

    lemma seqI [simp]:
    assumes "arr f" and "arr g" and "dom g = cod f"
    shows "seq g f"
    proof -
      have "ide (cod f) ∧ seq (cod f) f"
        using assms(1) has_codomain_iff_arr codomains_def cod_in_codomains ext by blast
      moreover have "ide (cod f) ∧ seq g (cod f)"
        using assms(2-3) domains_def domains_simp ext by fastforce
      ultimately show ?thesis
        using match_4 ide_def ext by metis
    qed

    text ‹
      This version of ‹seqI› is useful as an introduction rule, but not as useful
      as a simplification, because it requires finding the intermediary term ‹b›.
      Sometimes \emph{auto} is able to do this, but other times it is more expedient
      just to invoke this rule and fill in the missing terms manually, especially
      when dealing with a chain of compositions.
    ›

    lemma seqI' [intro]:
    assumes "«f : a → b»" and "«g : b → c»"
    shows "seq g f"
      using assms by fastforce

    lemma compatible_iff_seq:
    shows "domains g ∩ codomains f ≠ {} ⟷ seq g f"
    proof
      show "domains g ∩ codomains f ≠ {} ⟹ seq g f"
        using cod_in_codomains dom_in_domains empty_iff has_domain_iff_arr has_codomain_iff_arr
              domain_unique codomain_unique
        by (metis Int_emptyI seqI)
      show "seq g f ⟹ domains g ∩ codomains f ≠ {}"
      proof -
        assume gf: "seq g f"
        have 1: "cod f ∈ codomains f"
          using gf has_domain_iff_arr domains_comp cod_in_codomains codomains_simp by blast
        have "ide (cod f) ∧ seq (cod f) f"
          using 1 codomains_def ext by auto
        hence "seq g (cod f)"
          using gf has_domain_iff_arr match_2 domains_null ide_def by metis
        thus ?thesis
          using domains_def 1 codomains_def by auto
      qed
    qed

    text‹
      The following is another example of a crucial ``downward'' rule that would not be possible
      without a reserved @{term null} value.
›

    lemma seqE [elim]:
    assumes "seq g f"
    and "arr f ⟹ arr g ⟹ dom g = cod f ⟹ T"
    shows "T"
      using assms cod_in_codomains compatible_iff_seq has_domain_iff_arr has_codomain_iff_arr
            domains_comp codomains_comp domains_char codomain_unique
      by (metis Int_emptyI singletonD)

    lemma comp_in_homI [intro]:
    assumes "«f : a → b»" and "«g : b → c»"
    shows "«g ⋅ f : a → c»"
    proof
      show 1: "seq g f" using assms compatible_iff_seq by blast
      show "dom (g ⋅ f) = a"
        using assms 1 domains_comp domains_simp by blast
      show "cod (g ⋅ f) = c"
        using assms 1 codomains_comp codomains_simp by blast
    qed

    lemma comp_in_homI' [simp]:
    assumes "arr f" and "arr g" and "dom f = a" and "cod g = c" and "dom g = cod f"
    shows "«g ⋅ f : a → c»"
      using assms by auto

    lemma comp_in_homE [elim]:
    assumes "«g ⋅ f : a → c»"
    obtains b where "«f : a → b»" and "«g : b → c»"
      using assms in_hom_def domains_comp codomains_comp
      by (metis arrI in_homI seqE)

    text ‹
      The next two rules are useful as simplifications, but they slow down the
      simplifier too much to use them by default.  So it is necessary to guess when
      they are needed and cite them explicitly.  This is usually not too difficult.
    ›

    lemma comp_arr_dom:
    assumes "arr f" and "dom f = a"
    shows "f ⋅ a = f"
      using assms dom_in_domains has_domain_iff_arr domains_def ide_def by auto

    lemma comp_cod_arr:
    assumes "arr f" and "cod f = b"
    shows "b ⋅ f = f"
      using assms cod_in_codomains has_codomain_iff_arr ide_def codomains_def by auto

    lemma ide_char:
    shows "ide a ⟷ arr a ∧ dom a = a ∧ cod a = a"
      using ide_in_hom by auto

    text ‹
      In some contexts, this rule causes the simplifier to loop, but it is too useful
      not to have as a default simplification.  In cases where it is a problem, usually
      a method like \emph{blast} or \emph{force} will succeed if this rule is cited
      explicitly.
    ›

    lemma ideD [simp]:
    assumes "ide a"
    shows "arr a" and "dom a = a" and "cod a = a"
      using assms ide_char by auto

    lemma ide_dom [simp]:
    assumes "arr f"
    shows "ide (dom f)"
      using assms dom_in_domains has_domain_iff_arr domains_def by auto

    lemma ide_cod [simp]:
    assumes "arr f"
    shows "ide (cod f)"
      using assms cod_in_codomains has_codomain_iff_arr codomains_def by auto

    lemma dom_eqI:
    assumes "ide a" and "seq f a"
    shows "dom f = a"
      using assms cod_in_codomains codomain_unique ide_char
      by (metis seqE)

    lemma cod_eqI:
    assumes "ide b" and "seq b f"
    shows "cod f = b"
      using assms dom_in_domains domain_unique ide_char
      by (metis seqE)

    lemma dom_eqI':
    assumes "a ∈ domains f"
    shows "a = dom f"
      using assms dom_in_domains domain_unique by blast

    lemma cod_eqI':
    assumes "a ∈ codomains f"
    shows "a = cod f"
      using assms cod_in_codomains codomain_unique by blast

    lemma ide_char':
    shows "ide a ⟷ arr a ∧ (dom a = a ∨ cod a = a)"
      using ide_dom ide_cod ide_char by metis

    lemma dom_dom:
    assumes "arr f"
    shows "dom (dom f) = dom f"
      using assms by simp

    lemma cod_cod:
    assumes "arr f"
    shows "cod (cod f) = cod f"
      using assms by simp

    lemma dom_cod:
    assumes "arr f"
    shows "dom (cod f) = cod f"
      using assms by simp

    lemma cod_dom:
    assumes "arr f"
    shows "cod (dom f) = dom f"
      using assms by simp

    lemma dom_comp [simp]:
    assumes "seq g f"
    shows "dom (g ⋅ f) = dom f"
      using assms by (simp add: dom_def domains_comp)

    lemma cod_comp [simp]:
    assumes "seq g f"
    shows "cod (g ⋅ f) = cod g"
      using assms by (simp add: cod_def codomains_comp)

    lemma comp_ide_self [simp]:
    assumes "ide a"
    shows "a ⋅ a = a"
      using assms comp_arr_ide arrI by auto

    lemma ide_compE [elim]:
    assumes "ide (g ⋅ f)"
    and "seq g f ⟹ seq f g ⟹ g ⋅ f = dom f ⟹ g ⋅ f = cod g ⟹ T"
    shows "T"
      using assms dom_comp cod_comp ide_char ide_in_hom
      by (metis seqE seqI)

    text ‹
      The next two results are sometimes useful for performing manipulations at the
      head of a chain of composed arrows.  I have adopted the convention that such
      chains are canonically represented in right-associated form.  This makes it
      easy to perform manipulations at the ``tail'' of a chain, but more difficult
      to perform them at the ``head''.  These results take care of the rote manipulations
      using associativity that are needed to either permute or combine arrows at the
      head of a chain.
›

    lemma comp_permute:
    assumes "f ⋅ g = k ⋅ l" and "seq f g" and "seq g h"
    shows "f ⋅ g ⋅ h = k ⋅ l ⋅ h"
      using assms by (metis comp_assoc)

    lemma comp_reduce:
    assumes "f ⋅ g = k" and "seq f g" and "seq g h"
    shows "f ⋅ g ⋅ h = k ⋅ h"
      using assms comp_assoc by auto

    text‹
      Here we define some common configurations of arrows.
      These are defined as abbreviations, because we want all ``diagrammatic'' assumptions
      in a theorem to reduce readily to a conjunction of assertions of the basic forms
      @{term "arr f"}, @{term "dom f = X"}, @{term "cod f = Y"}, and @{term "in_hom f a b"}.
›

    abbreviation endo
    where "endo f ≡ seq f f"
     
    abbreviation antipar
    where "antipar f g ≡ seq g f ∧ seq f g"

    abbreviation span
    where "span f g ≡ arr f ∧ arr g ∧ dom f = dom g"

    abbreviation cospan
    where "cospan f g ≡ arr f ∧ arr g ∧ cod f = cod g"

    abbreviation par
    where "par f g ≡ arr f ∧ arr g ∧ dom f = dom g ∧ cod f = cod g"

  end

end

(*  Title:       ConcreteCategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2019
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter "Concrete Categories"

text ‹
  In this section we define a locale ‹concrete_category›, which provides a uniform
  (and more traditional) way to construct a category from specified sets of objects and arrows,
  with specified identity objects and composition of arrows.
  We prove that the identities and arrows of the constructed category are appropriately
  in bijective correspondence with the given sets and that domains, codomains, and composition
  in the constructed category are as expected according to this correspondence.
  In the later theory ‹Functor›, once we have defined functors and isomorphisms of categories,
  we will show a stronger property of this construction: if ‹C› is any category,
  then ‹C› is isomorphic to the concrete category formed from it in the obvious way by taking
  the identities of ‹C› as objects, the set of arrows of ‹C› as arrows, the identities of
  ‹C› as identity objects, and defining composition of arrows using the composition of ‹C›.
  Thus no information about ‹C› is lost by extracting its objects, arrows, identities, and
  composition and rebuilding it as a concrete category.
  We note, however, that we do not assume that the composition function given as parameter
  to the concrete category construction is ``extensional'', so in general it will contain
  incidental information about composition of non-composable arrows, and this information
  is not preserved by the concrete category construction.
›

theory ConcreteCategory
imports Category
begin

  locale concrete_category =
    fixes Obj :: "'o set"
    and Hom :: "'o ⇒ 'o ⇒ 'a set"
    and Id :: "'o ⇒ 'a"
    and Comp :: "'o ⇒ 'o ⇒ 'o ⇒ 'a ⇒ 'a ⇒'a"
    assumes Id_in_Hom: "A ∈ Obj ⟹ Id A ∈ Hom A A"
    and Comp_in_Hom: "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj; f ∈ Hom A B; g ∈ Hom B C ⟧
                         ⟹ Comp C B A g f ∈ Hom A C"
    and Comp_Hom_Id: "⟦ A ∈ Obj; f ∈ Hom A B ⟧ ⟹ Comp B A A f (Id A) = f"
    and Comp_Id_Hom: "⟦ B ∈ Obj; f ∈ Hom A B ⟧ ⟹ Comp B B A (Id B) f = f"
    and Comp_assoc: "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj; D ∈ Obj;
                       f ∈ Hom A B; g ∈ Hom B C; h ∈ Hom C D ⟧ ⟹
                        Comp D C A h (Comp C B A g f) = Comp D B A (Comp D C B h g) f"
  begin

    datatype ('oo, 'aa) arr =
      Null
    | MkArr 'oo 'oo 'aa

    abbreviation MkIde :: "'o ⇒ ('o, 'a) arr"
    where "MkIde A ≡ MkArr A A (Id A)"

    fun Dom :: "('o, 'a) arr ⇒ 'o"
    where "Dom (MkArr A _ _) = A"
        | "Dom _ = undefined"

    fun Cod
    where "Cod (MkArr _ B _) = B"
        | "Cod _ = undefined"

    fun Map
    where "Map (MkArr _ _ F) = F"
        | "Map _ = undefined"

    abbreviation Arr
    where "Arr f ≡ f ≠ Null ∧ Dom f ∈ Obj ∧ Cod f ∈ Obj ∧ Map f ∈ Hom (Dom f) (Cod f)"

    abbreviation Ide
    where "Ide a ≡ a ≠ Null ∧ Dom a ∈ Obj ∧ Cod a = Dom a ∧ Map a = Id (Dom a)"

    (*
     * Here we use COMP in order that uses of this locale can declare themselves as
     * sublocales and then define the abbreviation comp ≡ COMP.
     *)
    definition COMP :: "('o, 'a) arr comp"
    where "COMP g f ≡ if Arr f ∧ Arr g ∧ Dom g = Cod f then
                         MkArr (Dom f) (Cod g) (Comp (Cod g) (Dom g) (Dom f) (Map g) (Map f))
                      else
                         Null"

    interpretation partial_magma COMP
      using COMP_def by (unfold_locales, metis)

    lemma null_char:
    shows "null = Null"
    proof -
      let ?P = "λn. ∀f. COMP n f = n ∧ COMP f n = n"
      have "Null = null"
        using COMP_def null_def the1_equality [of ?P]
        by (metis (no_types, lifting))
      thus ?thesis by simp
    qed

    lemma ide_char:
    shows "ide f ⟷ Ide f"
    proof
      assume f: "Ide f"
      show "ide f"
      proof -
        have "COMP f f ≠ null"
          using f COMP_def null_char Id_in_Hom by auto
        moreover have "∀g. (COMP g f ≠ null ⟶ COMP g f = g) ∧
                           (COMP f g ≠ null ⟶ COMP f g = g)"
        proof (intro allI conjI)
          fix g
          show "COMP g f ≠ null ⟶ COMP g f = g"
            using f COMP_def null_char Comp_Hom_Id Id_in_Hom
            by (cases g, auto)
          show "COMP f g ≠ null ⟶ COMP f g = g"
            using f COMP_def null_char Comp_Id_Hom Id_in_Hom
            by (cases g, auto)
        qed
        ultimately show ?thesis
          using ide_def by blast
      qed
      next
      assume f: "ide f"
      have 1: "Arr f ∧ Dom f = Cod f"
        using f ide_def COMP_def null_char by metis
      moreover have "Map f = Id (Dom f)"
      proof -
        let ?g = "MkIde (Dom f)"
        have g: "Arr f ∧ Arr ?g ∧ Dom ?g = Cod f"
          using 1 Id_in_Hom
          by (intro conjI, simp_all)
        have "COMP ?g f = MkArr (Dom f) (Dom f) (Map f)"
          using g COMP_def Comp_Id_Hom by auto
        moreover have "COMP ?g f = ?g"
        proof -
          have "COMP ?g f ≠ null"
            using g 1 COMP_def null_char by simp
          thus ?thesis
            using f ide_def by blast
        qed
        ultimately show ?thesis by simp
      qed
      ultimately show "Ide f" by auto
    qed

    lemma ide_MkIde [simp]:
    assumes "A ∈ Obj"
    shows "ide (MkIde A)"
      using assms ide_char Id_in_Hom by simp

    lemma in_domains_char:
    shows "a ∈ domains f ⟷ Arr f ∧ a = MkIde (Dom f)"
    proof
      assume a: "a ∈ domains f"
      have "Ide a"
        using a domains_def ide_char COMP_def null_char by auto
      moreover have "Arr f ∧ Dom f = Cod a"
      proof -
        have "COMP f a ≠ null"
          using a domains_def by simp
        thus ?thesis
          using a domains_def COMP_def [of f a] null_char by metis
      qed
      ultimately show "Arr f ∧ a = MkIde (Dom f)"
        by (cases a, auto)
      next
      assume a: "Arr f ∧ a = MkIde (Dom f)"
      show "a ∈ domains f"
        using a Id_in_Hom COMP_def null_char domains_def by auto
    qed

    lemma in_codomains_char:
    shows "b ∈ codomains f ⟷ Arr f ∧ b = MkIde (Cod f)"
    proof
      assume b: "b ∈ codomains f"
      have "Ide b"
        using b codomains_def ide_char COMP_def null_char by auto
      moreover have "Arr f ∧ Dom b = Cod f"
      proof -
        have "COMP b f ≠ null"
          using b codomains_def by simp
        thus ?thesis
          using b codomains_def COMP_def [of b f] null_char by metis
      qed
      ultimately show "Arr f ∧ b = MkIde (Cod f)"
        by (cases b, auto)
      next
      assume b: "Arr f ∧ b = MkIde (Cod f)"
      show "b ∈ codomains f"
        using b Id_in_Hom COMP_def null_char codomains_def by auto
    qed

    lemma arr_char:
    shows "arr f ⟷ Arr f"
      using arr_def in_domains_char in_codomains_char by auto

    lemma arrI:
    assumes "f ≠ Null" and "Dom f ∈ Obj" "Cod f ∈ Obj" "Map f ∈ Hom (Dom f) (Cod f)"
    shows "arr f"
      using assms arr_char by blast

    lemma arrE:
    assumes "arr f"
    and "⟦ f ≠ Null; Dom f ∈ Obj; Cod f ∈ Obj; Map f ∈ Hom (Dom f) (Cod f) ⟧ ⟹ T"
    shows T
      using assms arr_char by simp

    lemma arr_MkArr [simp]:
    assumes "A ∈ Obj" and "B ∈ Obj" and "f ∈ Hom A B"
    shows "arr (MkArr A B f)"
      using assms arr_char by simp

    lemma MkArr_Map:
    assumes "arr f"
    shows "MkArr (Dom f) (Cod f) (Map f) = f"
      using assms arr_char by (cases f, auto)

    lemma Arr_comp:
    assumes "arr f" and "arr g" and "Dom g = Cod f"
    shows "Arr (COMP g f)"
      unfolding COMP_def
      using assms arr_char Comp_in_Hom by simp

    lemma Dom_comp [simp]:
    assumes "arr f" and "arr g" and "Dom g = Cod f"
    shows "Dom (COMP g f) = Dom f"
      unfolding COMP_def
      using assms arr_char by simp

    lemma Cod_comp [simp]:
    assumes "arr f" and "arr g" and "Dom g = Cod f"
    shows "Cod (COMP g f) = Cod g"
      unfolding COMP_def
      using assms arr_char by simp

    lemma Map_comp [simp]:
    assumes "arr f" and "arr g" and "Dom g = Cod f"
    shows "Map (COMP g f) = Comp (Cod g) (Dom g) (Dom f) (Map g) (Map f)"
      unfolding COMP_def
      using assms arr_char by simp

    lemma seq_char:
    shows "seq g f ⟷ arr f ∧ arr g ∧ Dom g = Cod f"
      using arr_char not_arr_null null_char COMP_def Arr_comp by metis

    interpretation category COMP
    proof
      show "⋀g f. COMP g f ≠ null ⟹ seq g f"
        using arr_char COMP_def null_char Comp_in_Hom by auto
      show 1: "⋀f. (domains f ≠ {}) = (codomains f ≠ {})"
        using in_domains_char in_codomains_char by auto
      show "⋀f g h. seq h g ⟹ seq (COMP h g) f ⟹ seq g f"
        by (auto simp add: seq_char)
      show "⋀f g h. seq h (COMP g f) ⟹ seq g f ⟹ seq h g"
        using seq_char COMP_def Comp_in_Hom by (metis Cod_comp)
      show "⋀f g h. seq g f ⟹ seq h g ⟹ seq (COMP h g) f"
        using Comp_in_Hom
        by (auto simp add: COMP_def seq_char)
      show "⋀g f h. seq g f ⟹ seq h g ⟹ COMP (COMP h g) f = COMP h (COMP g f)"
        using seq_char COMP_def Comp_assoc Comp_in_Hom Dom_comp Cod_comp Map_comp
        by auto
    qed

    proposition is_category:
    shows "category COMP"
      ..

    text ‹
      Functions ‹Dom›, ‹Cod›, and ‹Map› establish a correspondence between the
      arrows of the constructed category and the elements of the originally given
      parameters ‹Obj› and ‹Hom›.
    ›

    lemma Dom_in_Obj:
    assumes "arr f"
    shows "Dom f ∈ Obj"
      using assms arr_char by simp

    lemma Cod_in_Obj:
    assumes "arr f"
    shows "Cod f ∈ Obj"
      using assms arr_char by simp

    lemma Map_in_Hom:
    assumes "arr f"
    shows "Map f ∈ Hom (Dom f) (Cod f)"
      using assms arr_char by simp

    lemma MkArr_in_hom:
    assumes "A ∈ Obj" and "B ∈ Obj" and "f ∈ Hom A B"
    shows "in_hom (MkArr A B f) (MkIde A) (MkIde B)"
      using assms arr_char ide_MkIde
      by (simp add: in_codomains_char in_domains_char in_hom_def)

    text ‹
      The next few results show that domains, codomains, and composition in the constructed
      category are as expected according to the just-given correspondence.
    ›

    lemma dom_char:
    shows "dom f = (if arr f then MkIde (Dom f) else null)"
      using dom_def in_domains_char dom_in_domains has_domain_iff_arr by auto

    lemma cod_char:
    shows "cod f = (if arr f then MkIde (Cod f) else null)"
      using cod_def in_codomains_char cod_in_codomains has_codomain_iff_arr by auto

    lemma comp_char:
    shows "COMP g f = (if seq g f then
                         MkArr (Dom f) (Cod g) (Comp (Cod g) (Dom g) (Dom f) (Map g) (Map f))
                       else
                         null)"
      using COMP_def seq_char arr_char null_char by auto

    lemma in_hom_char:
    shows "in_hom f a b ⟷ arr f ∧ ide a ∧ ide b ∧ Dom f = Dom a ∧ Cod f = Dom b"
    proof
      show "in_hom f a b ⟹ arr f ∧ ide a ∧ ide b ∧ Dom f = Dom a ∧ Cod f = Dom b"
        using arr_char dom_char cod_char by auto
      show "arr f ∧ ide a ∧ ide b ∧ Dom f = Dom a ∧ Cod f = Dom b ⟹ in_hom f a b"
        using arr_char dom_char cod_char ide_char Id_in_Hom MkArr_Map in_homI by metis
    qed

    lemma Dom_dom [simp]:
    assumes "arr f"
    shows "Dom (dom f) = Dom f"
      using assms MkArr_Map dom_char by simp

    lemma Cod_dom [simp]:
    assumes "arr f"
    shows "Cod (dom f) = Dom f"
      using assms MkArr_Map dom_char by simp

    lemma Dom_cod [simp]:
    assumes "arr f"
    shows "Dom (cod f) = Cod f"
      using assms MkArr_Map cod_char by simp

    lemma Cod_cod [simp]:
    assumes "arr f"
    shows "Cod (cod f) = Cod f"
      using assms MkArr_Map cod_char by simp

    lemma Map_dom [simp]:
    assumes "arr f"
    shows "Map (dom f) = Id (Dom f)"
      using assms MkArr_Map dom_char by simp

    lemma Map_cod [simp]:
    assumes "arr f"
    shows "Map (cod f) = Id (Cod f)"
      using assms MkArr_Map cod_char by simp

    lemma Map_ide:
    assumes "ide a"
    shows "Map a = Id (Dom a)" and "Map a = Id (Cod a)"
      using assms ide_char dom_char [of a] Map_dom Map_cod ideD(1) by metis+

    (*
     * TODO: The next two ought to be simps, but they cause looping when they find themselves
     * in combination with dom_char and cod_char.
     *)
    lemma MkIde_Dom:
    assumes "arr a"
    shows "MkIde (Dom a) = dom a"
      using assms arr_char dom_char by (cases a, auto)

    lemma MkIde_Cod:
    assumes "arr a"
    shows "MkIde (Cod a) = cod a"
      using assms arr_char cod_char by (cases a, auto)

    lemma MkIde_Dom' [simp]:
    assumes "ide a"
    shows "MkIde (Dom a) = a"
      using assms MkIde_Dom by simp

    lemma MkIde_Cod' [simp]:
    assumes "ide a"
    shows "MkIde (Cod a) = a"
      using assms MkIde_Cod by simp

    lemma dom_MkArr [simp]:
    assumes "arr (MkArr A B F)"
    shows "dom (MkArr A B F) = MkIde A"
      using assms dom_char by simp

    lemma cod_MkArr [simp]:
    assumes "arr (MkArr A B F)"
    shows "cod (MkArr A B F) = MkIde B"
      using assms cod_char by simp

    lemma comp_MkArr [simp]:
    assumes "arr (MkArr A B F)" and "arr (MkArr B C G)"
    shows "COMP (MkArr B C G) (MkArr A B F) = MkArr A C (Comp C B A G F)"
      using assms comp_char [of "MkArr B C G" "MkArr A B F"] by simp

    text ‹
      The set ‹Obj› of ``objects'' given as a parameter is in bijective correspondence
      (via function ‹MkIde›) with the set of identities of the resulting category.
    ›

    proposition bij_betw_ide_Obj:
    shows "MkIde ∈ Obj → Collect ide"
    and "Dom ∈ Collect ide → Obj"
    and "A ∈ Obj ⟹ Dom (MkIde A) = A"
    and "a ∈ Collect ide ⟹ MkIde (Dom a) = a"
    and "bij_betw Dom (Collect ide) Obj"
    proof -
      show "MkIde ∈ Obj → Collect ide"
        using ide_MkIde by simp
      moreover show "Dom ∈ Collect ide → Obj"
        using arr_char ideD(1) by simp
      moreover show "⋀A. A ∈ Obj ⟹ Dom (MkIde A) = A"
        by simp
      moreover show "⋀a. a ∈ Collect ide ⟹ MkIde (Dom a) = a"
        using MkIde_Dom by simp
      ultimately show "bij_betw Dom (Collect ide) Obj"
        using bij_betwI by blast
    qed

    text ‹
      For each pair of identities ‹a› and ‹b›, the set ‹Hom (Dom a) (Dom b)› is in
      bijective correspondence (via function ‹MkArr (Dom a) (Dom b)›) with the
      ``hom-set'' ‹hom a b› of the resulting category.
    ›

    proposition bij_betw_hom_Hom:
    assumes "ide a" and "ide b"
    shows "Map ∈ hom a b → Hom (Dom a) (Dom b)"
    and "MkArr (Dom a) (Dom b) ∈ Hom (Dom a) (Dom b) → hom a b"
    and "⋀f. f ∈ hom a b ⟹ MkArr (Dom a) (Dom b) (Map f) = f"
    and "⋀F. F ∈ Hom (Dom a) (Dom b) ⟹ Map (MkArr (Dom a) (Dom b) F) = F"
    and "bij_betw Map (hom a b) (Hom (Dom a) (Dom b))"
    proof -
      show "Map ∈ hom a b → Hom (Dom a) (Dom b)"
        using Map_in_Hom cod_char dom_char in_hom_char by fastforce
      moreover show "MkArr (Dom a) (Dom b) ∈ Hom (Dom a) (Dom b) → hom a b"
        using assms Dom_in_Obj MkArr_in_hom [of "Dom a" "Dom b"] by simp
      moreover show "⋀f. f ∈ hom a b ⟹ MkArr (Dom a) (Dom b) (Map f) = f"
        using MkArr_Map by auto
      moreover show "⋀F. F ∈ Hom (Dom a) (Dom b)
                            ⟹ Map (MkArr (Dom a) (Dom b) F) = F"
        by simp
      ultimately show "bij_betw Map (hom a b) (Hom (Dom a) (Dom b))"
        using bij_betwI by blast
    qed

    lemma arr_eqI:
    assumes "arr t" and "arr t'" and "Dom t = Dom t'" and "Cod t = Cod t'" and "Map t = Map t'"
    shows "t = t'"
      using assms MkArr_Map by metis

  end

  sublocale concrete_category ⊆ category COMP
    using is_category by auto

end

(*  Title:       FreeCategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2016
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter FreeCategory

theory FreeCategory
imports Category ConcreteCategory
begin

  text‹
    This theory defines locales for constructing the free category generated by
    a graph, as well as some special cases, including the discrete category generated
    by a set of objects, the ``quiver'' generated by a set of arrows, and a ``parallel pair''
    of arrows, which is the diagram shape required for equalizers.
    Other diagram shapes can be constructed in a similar fashion.
›

  section Graphs

  text‹
    The following locale gives a definition of graphs in a traditional style.
›

  locale graph =
  fixes Obj :: "'obj set"
  and Arr :: "'arr set"
  and Dom :: "'arr ⇒ 'obj"
  and Cod :: "'arr ⇒ 'obj"
  assumes dom_is_obj: "x ∈ Arr ⟹ Dom x ∈ Obj"
  and cod_is_obj: "x ∈ Arr ⟹ Cod x ∈ Obj"
  begin

    text‹
      The list of arrows @{term p} forms a path from object @{term x} to object @{term y}
      if the domains and codomains of the arrows match up in the expected way.
›

    definition path
    where "path x y p ≡ (p = [] ∧ x = y ∧ x ∈ Obj) ∨
                        (p ≠ [] ∧ x = Dom (hd p) ∧ y = Cod (last p) ∧
                        (∀n. n ≥ 0 ∧ n < length p ⟶ nth p n ∈ Arr) ∧
                        (∀n. n ≥ 0 ∧ n < (length p)-1 ⟶ Cod (nth p n) = Dom (nth p (n+1))))"

    lemma path_Obj:
    assumes "x ∈ Obj"
    shows "path x x []"
      using assms path_def by simp

    lemma path_single_Arr:
    assumes "x ∈ Arr"
    shows "path (Dom x) (Cod x) [x]"
      using assms path_def by simp

    lemma path_concat:
    assumes "path x y p" and "path y z q"
    shows "path x z (p @ q)"
    proof -
      have "p = [] ∨ q = [] ⟹ ?thesis"
        using assms path_def by auto
      moreover have "p ≠ [] ∧ q ≠ [] ⟹ ?thesis"
      proof -
        assume pq: "p ≠ [] ∧ q ≠ []"
        have Cod_last: "Cod (last p) = Cod (nth (p @ q) ((length p)-1))"
          using assms pq by (simp add: last_conv_nth nth_append)
        moreover have Dom_hd: "Dom (hd q) = Dom (nth (p @ q) (length p))"
          using assms pq by (simp add: hd_conv_nth less_not_refl2 nth_append)
        show ?thesis
        proof -
          have 1: "⋀n. n ≥ 0 ∧ n < length (p @ q) ⟹ nth (p @ q) n ∈ Arr"
          proof -
            fix n
            assume n: "n ≥ 0 ∧ n < length (p @ q)"
            have "(n ≥ 0 ∧ n < length p) ∨ (n ≥ length p ∧ n < length (p @ q))"
              using n by auto
            thus "nth (p @ q) n ∈ Arr"
              using assms pq nth_append path_def le_add_diff_inverse length_append
                    less_eq_nat.simps(1) nat_add_left_cancel_less
              by metis
          qed
          have 2: "⋀n. n ≥ 0 ∧ n < length (p @ q) - 1 ⟹
                                    Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
          proof -
            fix n
            assume n: "n ≥ 0 ∧ n < length (p @ q) - 1"
            have 1: "(n ≥ 0 ∧ n < (length p) - 1) ∨ (n ≥ length p ∧ n < length (p @ q) - 1)
                       ∨ n = (length p) - 1"
              using n by auto
            thus "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
            proof -
              have "n ≥ 0 ∧ n < (length p) - 1 ⟹ ?thesis"
                using assms pq nth_append path_def by (metis add_lessD1 less_diff_conv)
              moreover have "n = (length p) - 1 ⟹ ?thesis"
                using assms pq nth_append path_def Dom_hd Cod_last by simp
              moreover have "n ≥ length p ∧ n < length (p @ q) - 1 ⟹ ?thesis"
              proof -
                assume 1: "n ≥ length p ∧ n < length (p @ q) - 1"
                have "Cod (nth (p @ q) n) = Cod (nth q (n - length p))"
                  using 1 nth_append leD by metis
                also have "... = Dom (nth q (n - length p + 1))"
                  using 1 assms(2) path_def by auto
                also have "... = Dom (nth (p @ q) (n + 1))"
                  using 1 nth_append
                  by (metis Nat.add_diff_assoc2 ex_least_nat_le le_0_eq le_add1 le_neq_implies_less
                            le_refl le_trans length_0_conv pq)
                finally show "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n + 1))" by auto
              qed
              ultimately show ?thesis using 1 by auto
            qed
          qed
          show ?thesis
            unfolding path_def using assms pq path_def hd_append2 Cod_last Dom_hd 1 2
            by simp
        qed
      qed
      ultimately show ?thesis by auto
    qed

  end

  section "Free Categories"

  text‹
    The free category generated by a graph has as its arrows all triples @{term "MkArr x y p"},
    where @{term x} and @{term y} are objects and @{term p} is a path from @{term x} to @{term y}.
    We construct it here an instance of the general construction given by the
    @{locale concrete_category} locale.
›

  locale free_category =
    G: graph Obj Arr D C
  for Obj :: "'obj set"
  and Arr :: "'arr set"
  and D :: "'arr ⇒ 'obj"
  and C :: "'arr ⇒ 'obj"
  begin

    type_synonym ('o, 'a) arr = "('o, 'a list) concrete_category.arr"

    sublocale concrete_category ‹Obj :: 'obj set› ‹λx y. Collect (G.path x y)›
      ‹λ_. []› ‹λ_ _ _ g f. f @ g›
      using G.path_Obj G.path_concat
      by (unfold_locales, simp_all)

    abbreviation comp      (infixr "⋅" 55)
    where "comp ≡ COMP"
    notation in_hom     ("«_ : _ → _»")

    abbreviation Path
    where "Path ≡ Map"

    lemma arr_single [simp]:
    assumes "x ∈ Arr"
    shows "arr (MkArr (D x) (C x) [x])"
      using assms
      by (simp add: G.cod_is_obj G.dom_is_obj G.path_single_Arr)

  end

  section "Discrete Categories"

  text‹
    A discrete category is a category in which every arrow is an identity.
    We could construct it as the free category generated by a graph with no
    arrows, but it is simpler just to apply the @{locale concrete_category}
    construction directly.
›

  locale discrete_category =
  fixes Obj :: "'obj set"
  begin

    type_synonym 'o arr = "('o, unit) concrete_category.arr"

    sublocale concrete_category ‹Obj :: 'obj set› ‹λx y. if x = y then {x} else {}›
      ‹λx. x› ‹λ_ _ x _ _. x›
      apply unfold_locales
          apply simp_all
        apply (metis empty_iff)
       apply (metis empty_iff singletonD)
      by (metis empty_iff singletonD)

    abbreviation comp      (infixr "⋅" 55)
    where "comp ≡ COMP"
    notation in_hom        ("«_ : _ → _»")

    lemma is_discrete:
    shows "arr f ⟷ ide f"
      using ide_char arr_char by simp

    lemma arr_char:
    shows "arr f ⟷ Dom f ∈ Obj ∧ f = MkIde (Dom f)"
      using is_discrete
      by (metis (no_types, lifting) cod_char dom_char ide_MkIde ide_char ide_char')

    lemma arr_char':
    shows "arr f ⟷ f ∈ MkIde ` Obj"
      using arr_char image_iff by auto

    lemma dom_char:
    shows "dom f = (if arr f then f else null)"
      using dom_char is_discrete by simp

    lemma cod_char:
    shows "cod f = (if arr f then f else null)"
      using cod_char is_discrete by simp

    lemma in_hom_char:
    shows "«f : a → b» ⟷ arr f ∧ f = a ∧ f = b"
      using is_discrete by auto

    lemma seq_char:
    shows "seq g f ⟷ arr f ∧ f = g"
      using is_discrete
      by (metis (no_types, lifting) comp_arr_dom seqE dom_char)
    
    lemma comp_char:
    shows "g ⋅ f = (if seq g f then f else null)"
    proof -
      have "¬ seq g f ⟹ ?thesis"
        using comp_char by presburger
      moreover have "seq g f ⟹ ?thesis"
        using seq_char comp_char comp_arr_ide is_discrete
        by (metis (no_types, lifting))
      ultimately show ?thesis by blast
    qed

  end

  text‹
    The empty category is the discrete category generated by an empty set of objects.
›

  locale empty_category =
    discrete_category "{} :: unit set"
  begin

    lemma is_empty:
    shows "¬arr f"
      using arr_char by simp

  end

  section "Quivers"

  text‹
    A quiver is a two-object category whose non-identity arrows all point in the
    same direction.  A quiver is specified by giving the set of these non-identity arrows.
›

  locale quiver =
  fixes Arr :: "'arr set"
  begin

    type_synonym 'a arr = "(unit, 'a) concrete_category.arr"

    sublocale free_category "{False, True}" Arr "λ_. False" "λ_. True"
      by (unfold_locales, simp_all)

    notation comp                  (infixr "⋅" 55)
    notation in_hom                ("«_ : _ → _»")

    definition Zero
    where "Zero ≡ MkIde False"

    definition One
    where "One ≡ MkIde True"

    definition fromArr
    where "fromArr x ≡ if x ∈ Arr then MkArr False True [x] else null"

    definition toArr
    where "toArr f ≡ hd (Path f)"

    lemma ide_char:
    shows "ide f ⟷ f = Zero ∨ f = One"
    proof -
      have "ide f ⟷ f = MkIde False ∨ f = MkIde True"
        using ide_char concrete_category.MkIde_Dom' concrete_category_axioms by fastforce
      thus ?thesis
        using comp_def Zero_def One_def by simp
    qed

    lemma arr_char':
    shows "arr f ⟷ f =
           MkIde False ∨ f = MkIde True ∨ f ∈ (λx. MkArr False True [x]) ` Arr"
    proof
      assume f: "f = MkIde False ∨ f = MkIde True ∨ f ∈ (λx. MkArr False True [x]) ` Arr"
      show "arr f" using f by auto
      next
      assume f: "arr f"
      have "¬(f = MkIde False ∨ f = MkIde True) ⟹ f ∈ (λx. MkArr False True [x]) ` Arr"
      proof -
        assume f': "¬(f = MkIde False ∨ f = MkIde True)"
        have 0: "Dom f = False ∧ Cod f = True"
          using f f' arr_char G.path_def MkArr_Map by fastforce
        have 1: "f = MkArr False True (Path f)"
          using f 0 arr_char MkArr_Map by force
        moreover have "length (Path f) = 1"
        proof -
          have "length (Path f) ≠ 0"
            using f f' 0 arr_char G.path_def by simp
          moreover have "⋀x y p. length p > 1 ⟹ ¬ G.path x y p"
            using G.path_def less_diff_conv by fastforce
          ultimately show ?thesis
            using f arr_char
            by (metis less_one linorder_neqE_nat mem_Collect_eq)
        qed
        moreover have "⋀p. length p = 1 ⟷ (∃x. p = [x])"
          by (auto simp: length_Suc_conv)
        ultimately have "∃x. x ∈ Arr ∧ Path f = [x]"
          using f G.path_def arr_char
          by (metis (no_types, lifting) Cod.simps(1) Dom.simps(1) le_eq_less_or_eq
              less_numeral_extra(1) mem_Collect_eq nth_Cons_0)
        thus "f ∈ (λx. MkArr False True [x]) ` Arr"
          using 1 by auto
      qed
      thus "f = MkIde False ∨ f = MkIde True ∨ f ∈ (λx. MkArr False True [x]) ` Arr"
        by auto
    qed

    lemma arr_char:
    shows "arr f ⟷ f = Zero ∨ f = One ∨ f ∈ fromArr ` Arr"
      using arr_char' Zero_def One_def fromArr_def by simp

    lemma dom_char:
    shows "dom f = (if arr f then
                      if f = One then One else Zero
                    else null)"
    proof -
      have "¬ arr f ⟹ ?thesis"
        using dom_char by simp
      moreover have "arr f ⟹ ?thesis"
      proof -
        assume f: "arr f"
        have 1: "dom f = MkIde (Dom f)"
          using f dom_char by simp
        have "f = One ⟹ ?thesis"
          using f 1 One_def by (metis (full_types) Dom.simps(1))
        moreover have "f = Zero ⟹ ?thesis"
          using f 1 Zero_def by (metis (full_types) Dom.simps(1))
        moreover have "f ∈ fromArr ` Arr ⟹ ?thesis"
          using f fromArr_def G.path_def Zero_def calculation(1) by auto
        ultimately show ?thesis
          using f arr_char by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma cod_char:
    shows "cod f = (if arr f then
                      if f = Zero then Zero else One
                    else null)"
    proof -
      have "¬ arr f ⟹ ?thesis"
        using cod_char by simp
      moreover have "arr f ⟹ ?thesis"
      proof -
        assume f: "arr f"
        have 1: "cod f = MkIde (Cod f)"
          using f cod_char by simp
        have "f = One ⟹ ?thesis"
          using f 1 One_def by (metis (full_types) Cod.simps(1) f)
        moreover have "f = Zero ⟹ ?thesis"
          using f 1 Zero_def by (metis (full_types) Cod.simps(1) f)
        moreover have "f ∈ fromArr ` Arr ⟹ ?thesis"
          using f fromArr_def G.path_def One_def calculation(2) by auto
        ultimately show ?thesis
          using f arr_char by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma seq_char:
    shows "seq g f ⟷ arr g ∧ arr f ∧ ((f = Zero ∧ g ≠ One) ∨ (f ≠ Zero ∧ g = One))"
    proof
      assume gf: "arr g ∧ arr f ∧ ((f = Zero ∧ g ≠ One) ∨ (f ≠ Zero ∧ g = One))"
      show "seq g f"
        using gf dom_char cod_char by auto
      next
      assume gf: "seq g f"
      hence 1: "arr f ∧ arr g ∧ dom g = cod f" by auto
      have "Cod f = False ⟹ f = Zero"
        using gf 1 arr_char [of f] G.path_def Zero_def One_def cod_char Dom_cod
        by (metis (no_types, lifting) Dom.simps(1))
      moreover have "Cod f = True ⟹ g = One"
        using gf 1 arr_char [of f] G.path_def Zero_def One_def dom_char Dom_cod
        by (metis (no_types, lifting) Dom.simps(1))
      moreover have "¬(f = MkIde False ∧ g = MkIde True)"
        using 1 by auto
      ultimately show "arr g ∧ arr f ∧ ((f = Zero ∧ g ≠ One) ∨ (f ≠ Zero ∧ g = One))"
        using gf arr_char One_def Zero_def by blast
    qed

    lemma not_ide_fromArr:
    shows "¬ ide (fromArr x)"
      using fromArr_def ide_char ide_def Zero_def One_def
      by (metis Cod.simps(1) Dom.simps(1))

    lemma in_hom_char:
    shows "«f : a → b» ⟷ (a = Zero ∧ b = Zero ∧ f = Zero) ∨
                            (a = One ∧ b = One ∧ f = One) ∨
                            (a = Zero ∧ b = One ∧ f ∈ fromArr ` Arr)"
    proof -
      have "f = Zero ⟹ ?thesis"
        using arr_char' [of f] ide_char'
        by (metis (no_types, lifting) Zero_def category.in_homE category.in_homI
            cod_MkArr dom_MkArr imageE is_category not_ide_fromArr)
      moreover have "f = One ⟹ ?thesis"
        using arr_char' [of f] ide_char'
        by (metis (no_types, lifting) One_def category.in_homE category.in_homI
            cod_MkArr dom_MkArr image_iff is_category not_ide_fromArr)
      moreover have "f ∈ fromArr ` Arr ⟹ ?thesis"
      proof -
        assume f: "f ∈ fromArr ` Arr"
        have 1: "arr f" using f arr_char by simp
        moreover have "dom f = Zero ∧ cod f = One"
          using f 1 arr_char dom_char cod_char fromArr_def
          by (metis (no_types, lifting) ide_char imageE not_ide_fromArr)
        ultimately have "in_hom f Zero One" by auto
        thus "in_hom f a b ⟷ (a = Zero ∧ b = Zero ∧ f = Zero ∨
                                           a = One ∧ b = One ∧ f = One ∨
                                           a = Zero ∧ b = One ∧ f ∈ fromArr ` Arr)"
          using f ide_char by auto
      qed
      ultimately show ?thesis
        using arr_char [of f] by fast
    qed

    lemma Zero_not_eq_One [simp]:
    shows "Zero ≠ One"
      by (simp add: One_def Zero_def)

    lemma Zero_not_eq_fromArr [simp]:
    shows "Zero ∉ fromArr ` Arr"
      using ide_char not_ide_fromArr
      by (metis (no_types, lifting) image_iff)

    lemma One_not_eq_fromArr [simp]:
    shows "One ∉ fromArr ` Arr"
      using ide_char not_ide_fromArr
      by (metis (no_types, lifting) image_iff)

    lemma comp_char:
    shows "g ⋅ f = (if seq g f then
                      if f = Zero then g else if g = One then f else null
                    else null)"
    proof -
      have "seq g f ⟹ f = Zero ⟹ g ⋅ f = g"
        using seq_char comp_char [of g f] Zero_def dom_char cod_char comp_arr_dom
        by auto
      moreover have "seq g f ⟹ g = One ⟹ g ⋅ f = f"
        using seq_char comp_char [of g f] One_def dom_char cod_char comp_cod_arr
        by simp
      moreover have "seq g f ⟹ f ≠ Zero ⟹ g ≠ One ⟹ g ⋅ f = null"
        using seq_char Zero_def One_def by simp
      moreover have "¬seq g f ⟹ g ⋅ f = null"
        using comp_char ext by fastforce
      ultimately show ?thesis by argo
    qed

    lemma comp_simp [simp]:
    assumes "seq g f"
    shows "f = Zero ⟹ g ⋅ f = g"
    and "g = One ⟹ g ⋅ f = f"
      using assms seq_char comp_char by metis+

    lemma arr_fromArr:
    assumes "x ∈ Arr"
    shows "arr (fromArr x)"
      using assms fromArr_def arr_char image_eqI by simp

    lemma toArr_in_Arr:
    assumes "arr f" and "¬ide f"
    shows "toArr f ∈ Arr"
    proof -
      have "⋀a. a ∈ Arr ⟹ Path (fromArr a) = [a]"
        using fromArr_def arr_char by simp
      hence "hd (Path f) ∈ Arr"
        using assms arr_char ide_char by auto
      thus ?thesis
        by (simp add: toArr_def)
    qed

    lemma toArr_fromArr [simp]:
    assumes "x ∈ Arr"
    shows "toArr (fromArr x) = x"
      using assms fromArr_def toArr_def
      by (simp add: toArr_def)

    lemma fromArr_toArr [simp]:
    assumes "arr f" and "¬ide f"
    shows "fromArr (toArr f) = f"
      using assms fromArr_def toArr_def arr_char ide_char toArr_fromArr by auto

  end

  section "Parallel Pairs"

  text‹
    A parallel pair is a quiver with two non-identity arrows.
    It is important in the definition of equalizers.
›

  locale parallel_pair =
    quiver "{False, True} :: bool set"
  begin

    typedef arr = "UNIV :: bool quiver.arr set" ..

    definition j0
    where "j0 ≡ fromArr False"

    definition j1
    where "j1 ≡ fromArr True"

    lemma arr_char:
    shows "arr f ⟷ f = Zero ∨ f = One ∨ f = j0 ∨ f = j1"
      using arr_char j0_def j1_def by simp

    lemma dom_char:
    shows "dom f = (if f = j0 ∨ f = j1 then Zero else if arr f then f else null)"
      using arr_char dom_char j0_def j1_def
      by (metis ide_char not_ide_fromArr)

    lemma cod_char:
    shows "cod f = (if f = j0 ∨ f = j1 then One else if arr f then f else null)"
      using arr_char cod_char j0_def j1_def
      by (metis ide_char not_ide_fromArr)

    lemma j0_not_eq_j1 [simp]:
    shows "j0 ≠ j1"
      using j0_def j1_def
      by (metis insert_iff toArr_fromArr)

    lemma Zero_not_eq_j0 [simp]:
    shows "Zero ≠ j0"
      using Zero_def j0_def Zero_not_eq_fromArr by auto

    lemma Zero_not_eq_j1 [simp]:
    shows "Zero ≠ j1"
      using Zero_def j1_def Zero_not_eq_fromArr by auto

    lemma One_not_eq_j0 [simp]:
    shows "One ≠ j0"
      using One_def j0_def One_not_eq_fromArr by auto

    lemma One_not_eq_j1 [simp]:
    shows "One ≠ j1"
      using One_def j1_def One_not_eq_fromArr by auto

    lemma dom_simp [simp]:
    shows "dom Zero = Zero"
    and "dom One = One"
    and "dom j0 = Zero"
    and "dom j1 = Zero"
      using dom_char arr_char by auto

    lemma cod_simp [simp]:
    shows "cod Zero = Zero"
    and "cod One = One"
    and "cod j0 = One"
    and "cod j1 = One"
      using cod_char arr_char by auto

  end

end